T:Type, R:(TT), n:, x, y:T.
(x rel_exp(T;R;n) y)  (L:T List. (||L|| = n+1 & rel-path-between(T;R;x;y;L))) 

latex

Definitions

x f y, (i = j), , x:AB(x), rel_exp(T;R;n), f(a), type List, , s = t, rel-path-between(T;R;x;y;L), x:A  B(x), P & Q, x:A. B(x), P  Q, x:A. B(x), Type, , {x:A| B(x)} , t  T, A  B, i  j , P  Q, False, A, #$n, -n, n+m, n - m, a < b, Void, P  Q, ||as||, b, last(L), rel-path(R;L), hd(l), <a, b>, , A c B, [], [car / cdr], i <z j, i z j, l[i], {i..j}, i  j < k, ff, b, tt, x =a y, null(as), a < b, a < b, [d], p  q, p  q, p q, Unit, left + right, x.A(x), A List, x:A.B(x), Top, S  T, True

Lemmas

rel-path-between-cons, null wf3, top wf, length cons, le wf, member wf, length wf1, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert of eq int, eq int wf, bool wf, bnot wf, not wf, non neg length, int seg wf, rel-path wf, last wf, assert wf, ge wf, nat properties, rel-path-between wf, rel exp wf, iff wf, nat wf, nat ind tp